wlan.5.jani:model: info: wlan.5 is an MDP model.
wlan.5.jani:variables[7]: info: Expanding variable "s1" into 12 locations in automaton "station1".
wlan.5.jani:variables[12]: info: Expanding variable "s2" into 12 locations in automaton "station2".
wlan.5.jani: info: Need 16 bytes per state.
wlan.5.jani: info: Explored 1295218 states for COL=0.
wlan.5.jani:properties[2]: warning: Computing minimum expected reward in property "cost_min" without checking for zero-reward end components.
Peak memory usage: 486 MB
Analysis results for wlan.5.jani
Experiment COL=0
+ State space exploration
State size: 16 bytes
States: 1295218
Transitions: 1646074
Branches: 2929960
Rate: 407943 states/s
Time: 3.3 s
+ Property cost_min
Value: 7625
Bounds: [7625, infinity)
Time: 100.6 s
+ Precomputations
Max. prob. 1 states: 1295218
Time for max. prob. 1 states: 100.0 s
+ Essential states
Iterations: 15
Essential states: 12350
Transitions: 20903
Branches: 254795
Time: 0.5 s
+ Value iteration
Final error: 0
Iterations: 8
Time: 0.0 s
Exported results to file "/out.txt".